In this chapter we introduce \ahopi, the core of calculi for higher-order concurrency such as
CHOCS \citep{Tho89}, Plain CHOCS \citep{Tho93}, and Higher-Order
$\pi$-calculus \citep{San923,San96H,San96int}.

The syntax and the semantics of the calculus are given in Section \ref{ss:hocore}.
Then, Section \ref{ss:core-expres} discusses the expressiveness of the language.
The main result is an encoding of Minsky machines into \hocore, which allows to 
infer that the language is Turing complete. 
Section \ref{ss:core-discus} provides some concluding remarks.


\section{The Calculus}\label{ss:hocore}


\paragraph{Syntax.}
We use $a,b,c$ to range over names (also called channels), and $x,y,z$ to
range over variables; the sets of names and variables are  disjoint.

\begin{mydefi}%[\hocore processes]
The set of \hocore processes is given by the following syntax:
\[
\begin{array}{rcll}
P,\,Q & :: = &  \out a P   & \mbox{output}\\[\mypt]
 & \midd &  \inp a x . P & \mbox{input prefix} \\[\mypt]
 & \midd &  x  & \mbox{process variable} \\[\mypt]
 & \midd &  P \parallel Q & \mbox{parallel composition} \\[\mypt]
 & \midd & \nil & \mbox{nil}\\[\mypt]
\end{array} 
 \]
 
\end{mydefi}


An input $\inp a x.P$ binds the free occurrences of $x$ in
$P$.
We write $\fv P$ for the set of free variables in $P$,  
and  $\bv P$ for the %set of its 
bound variables.  
We identify processes up to a renaming of bound
 variables.
A process is \emph{closed} if it does not have free variables. 
In a statement, a name is \emph{fresh} if it is not
 among the names of the objects (processes, actions, etc.) of the
statement. 
% We write $\PrOp$ for the set of all processes, and $\PrClo$ for the subset
% of {closed} processes.
We abbreviate $\inp a x . P$, with $x \not \in \fv P$, 
as $a . P$, $\out{a}{\nil}$ as $\overline{a}$,
and $P_1 \parallel \ldots \parallel P_k$ as $\prod_{i=1}^k \: P_i$. 
\iflong{
Similarly, we write $\prod^n_1 P$ as an abbreviation for the parallel composition of
$n$ copies of $P$. 
Further, $P{\sub {\til Q}\tilX}$ denotes the componentwise and simultaneous substitution of variables
${\tilX}$ with processes ${\til Q}$ in $P$ (we assume members of ${\tilX}$ are distinct).}{}

The size of a process is defined as follows. 
\begin{mydefi}%[Size of a process]
The \emph{size} of a process $P$, written $\size{P}$, is  inductively defined as:
\[
\begin{array}{c}
\size{\nil}=0 \qquad \size{P \parallel Q}=\size{P} + \size{Q} \qquad \size{x}=1\\ 
\size{\out a P}=1 + \size{P} \qquad \size{\inp a x . P}=1 + \size{P} 
\end{array}
\]
\end{mydefi}

\paragraph{Semantics.}
Now we describe the LTS, which is defined on open processes.
There are three forms of transitions: $\tau$ transitions $P  \arr\tau P'$;
input transitions $P \arr{\ia a x} P'$, meaning that  $P$
can receive   at  $a$ a process that
will replace $x$ in the continuation $P'$; and
output transitions $P \arr{\out  a {P'}}P''$ meaning that $P$ emits
$P'$ at $a$, and in doing so it
evolves to $P''$.
We use $\alpha $ to indicate a generic label of a transition. 
The notions of free and bound variables extend to labels as expected.
\[\mathrm{\textsc{Inp}}~~~{\inp a x. P} \arr{\ia a x  }  {P } \qquad \qquad \mathrm{\textsc{Out}}~~~{\out a  P } \arr{\out a P  }  {\nil}\]
\infrule{\textsc{Act1}~~}{P_1 \arr\alpha P_1' \andalso 
\bv \alpha \cap \fv{P_2} = \emptyset
}{
P_1 \parallel P_2 \arr\alpha P'_1 \parallel P_2 
} 
\infrule{\textsc{Tau1}}{P_1 \arr{\out a P} P_1' \andalso 
P_2 \arr{\iae a (x)} P'_2   
}{
P_1 \parallel P_2 \arr\tau  P'_1 \parallel P'_2 \sub{P}{x}}
% We write  $P \arr{\iae a M}Q $ if 
% $P \arr{\ia a x}Q' $ and $Q' \sub Mx = Q$ (this form of action is
% called  \emph{early input} in the literature).  
% In the remainder, $\alpha $ may also be an early input. 
% Further, with some abuse of notation, if $\alpha  = {\ia a x}$ then
% $\alpha \sub Qx = aQ$.
(We have omitted \textsc{Act2} and \textsc{Tau2}, the symmetric counterparts
of the last two rules.) 
 
% Finally we define  the \emph{barbs}, and write $P \dwa_a$ if there is
% $\alpha $ and $P'$ s.t.\
% $P \arr\alpha P'$ where $\alpha $ is an input or output action at $a$.

\begin{mydefi}%[Structural Congruence]
\label{d:struct} 
The \emph{structural congruence} relation  
is the smallest congruence 
generated by the following laws:\\
\iflong{$P \parallel \mathbf{0} \equiv P$, ~~$P_1 \parallel P_2 \equiv P_2 \parallel P_1$,~~$P_1 \parallel (P_2 \parallel P_3) \equiv (P_1 \parallel P_2) \parallel P_3$.}{$P \parallel \mathbf{0} \equiv P$, ~~$P_1 \parallel P_2 \equiv P_2 \parallel P_1$,\\$P_1 \parallel (P_2 \parallel P_3) \equiv (P_1 \parallel P_2) \parallel P_3$.}
 \end{mydefi} 
\emph{Reductions} $P \pired P'$ are defined as $P \equiv\arr{\tau}\equiv P'$.
\iflong{ We now state a few results which will be important later. 

\begin{lemma}\label{l:equiv}
If $P \arr \alpha P'$ and $P \equiv Q$ then there exists $Q'$ such that $Q \arr \alpha Q'$ and 
$P' \equiv Q'$.
\end{lemma}
\begin{proof}
%By induction on the transition $P \arr \alpha P'$.
%\as{Shouldn't we do the proof by 
By induction on the derivation of $P \equiv Q$, then by case analysis on $P \arr \alpha Q$.
%?}
\end{proof}

\begin{mydefi}
A variable $x$  \emph{is guarded in $P\in \PrOp$} (or simply \emph{guarded},
when $P$ is clear from the context) if  
$x $ only occurs free in an output or in 
subexpressions of $P$ of the form $\pi. P'$, where $\pi$ is any prefix. 
A process  $P\in\PrOp$ is {\em guarded} (or has
\emph{guarded variables}) if all its free variables 
are guarded.
\end{mydefi}

In particular, notice that if $x$ is guarded in $P$ then it does not appear in evaluation contexts
(i.e. contexts which allow transitions in the hole position), and if $x$ is not free in $P$ then it is guarded in $P$.
In the lemma below, we recall that an output action from an open process
 may contain free variables, thus $\alpha \sub {\til R}\tilX$ is the action obtained from
$\alpha$ by applying the substitution $\sub {\til R}\tilX$.

\begin{lemma}
\label{l:GUA}
Suppose that $P \in\PrOp$ 
and variables $\tilX$ are guarded in $P$.
% is guarded. 
Then, for all $\til R\in\PrOp$ we have:
\begin{enumerate}
\item  If $P \arr\alpha  P'$, 
%with bound variables in $\alpha $ fresh in $\til R$, 
with variables in $\til R$ disjoint from those in $P$, $\alpha$ and $\til x$,
then $P{\sub {\til R}\tilX}   \arr{\alpha{\sub {\til R}\tilX} } 
 P'  {\sub {\til R}\tilX}$; 

\item  If   $P{\sub {\til R}\tilX}   \arr{\alpha'} M'$, 
%with bound variables in $\alpha' $ fresh in $\til R$, 
with variables in $\til R$ disjoint from those in $P$, $\alpha'$ and $\til x$,
then  there is $P'$
such that  $P \arr{\alpha} P'$ and  $M' = P'{\sub {\til R}\tilX}$, $\alpha' = \alpha{\sub {\til R}\tilX}$. 
\end{enumerate}
 \end{lemma} 

\begin{proof}
By induction on the transitions.
\end{proof}

\begin{lemma}
\label{l:equiv_cont}
For all  $P\in\PrOp$ and $x$ 
there is $P'\in\PrOp$ with $x$ guarded in $P'$, and $n\geq 0$
 such that 
\begin{enumerate}
\item $P \equiv  P' \parallel  \prod^n_1 x$
\item $P{\sub Rx}\equiv  P'{\sub Rx} \parallel \prod^n_1  R$, for all $R\in\PrOp$.
\end{enumerate}
\end{lemma} 
\begin{proof}
By induction on the structure of processes.
\end{proof}
}{
}
